Problem:
 active(f(a(),X,X)) -> mark(f(X,b(),b()))
 active(b()) -> mark(a())
 active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
 f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
 proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
 proper(a()) -> ok(a())
 proper(b()) -> ok(b())
 f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 Complexity Transformation Processor:
  strict:
   active(f(a(),X,X)) -> mark(f(X,b(),b()))
   active(b()) -> mark(a())
   active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
   f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
   proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
   proper(a()) -> ok(a())
   proper(b()) -> ok(b())
   f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [top](x0) = x0 + 14,
     
     [ok](x0) = x0 + 3,
     
     [proper](x0) = x0 + 8,
     
     [mark](x0) = x0 + 8,
     
     [b] = 3,
     
     [active](x0) = x0 + 2,
     
     [f](x0, x1, x2) = x0 + x1 + x2 + 4,
     
     [a] = 9
    orientation:
     active(f(a(),X,X)) = 2X + 15 >= X + 18 = mark(f(X,b(),b()))
     
     active(b()) = 5 >= 17 = mark(a())
     
     active(f(X1,X2,X3)) = X1 + X2 + X3 + 6 >= X1 + X2 + X3 + 6 = f(X1,active(X2),X3)
     
     f(X1,mark(X2),X3) = X1 + X2 + X3 + 12 >= X1 + X2 + X3 + 12 = mark(f(X1,X2,X3))
     
     proper(f(X1,X2,X3)) = X1 + X2 + X3 + 12 >= X1 + X2 + X3 + 28 = f(proper(X1),proper(X2),proper(X3))
     
     proper(a()) = 17 >= 12 = ok(a())
     
     proper(b()) = 11 >= 6 = ok(b())
     
     f(ok(X1),ok(X2),ok(X3)) = X1 + X2 + X3 + 13 >= X1 + X2 + X3 + 7 = ok(f(X1,X2,X3))
     
     top(mark(X)) = X + 22 >= X + 22 = top(proper(X))
     
     top(ok(X)) = X + 17 >= X + 16 = top(active(X))
    problem:
     strict:
      active(f(a(),X,X)) -> mark(f(X,b(),b()))
      active(b()) -> mark(a())
      active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
      f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
      proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
      top(mark(X)) -> top(proper(X))
     weak:
      proper(a()) -> ok(a())
      proper(b()) -> ok(b())
      f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
      top(ok(X)) -> top(active(X))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [top](x0) = x0 + 4,
       
       [ok](x0) = x0,
       
       [proper](x0) = x0,
       
       [mark](x0) = x0 + 1,
       
       [b] = 13,
       
       [active](x0) = x0,
       
       [f](x0, x1, x2) = x0 + x1 + x2 + 4,
       
       [a] = 12
      orientation:
       active(f(a(),X,X)) = 2X + 16 >= X + 31 = mark(f(X,b(),b()))
       
       active(b()) = 13 >= 13 = mark(a())
       
       active(f(X1,X2,X3)) = X1 + X2 + X3 + 4 >= X1 + X2 + X3 + 4 = f(X1,active(X2),X3)
       
       f(X1,mark(X2),X3) = X1 + X2 + X3 + 5 >= X1 + X2 + X3 + 5 = mark(f(X1,X2,X3))
       
       proper(f(X1,X2,X3)) = X1 + X2 + X3 + 4 >= X1 + X2 + X3 + 4 = f(proper(X1),proper(X2),proper(X3))
       
       top(mark(X)) = X + 5 >= X + 4 = top(proper(X))
       
       proper(a()) = 12 >= 12 = ok(a())
       
       proper(b()) = 13 >= 13 = ok(b())
       
       f(ok(X1),ok(X2),ok(X3)) = X1 + X2 + X3 + 4 >= X1 + X2 + X3 + 4 = ok(f(X1,X2,X3))
       
       top(ok(X)) = X + 4 >= X + 4 = top(active(X))
      problem:
       strict:
        active(f(a(),X,X)) -> mark(f(X,b(),b()))
        active(b()) -> mark(a())
        active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
        f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
        proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
       weak:
        top(mark(X)) -> top(proper(X))
        proper(a()) -> ok(a())
        proper(b()) -> ok(b())
        f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
        top(ok(X)) -> top(active(X))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [top](x0) = x0 + 2,
         
         [ok](x0) = x0 + 2,
         
         [proper](x0) = x0 + 2,
         
         [mark](x0) = x0 + 2,
         
         [b] = 2,
         
         [active](x0) = x0 + 2,
         
         [f](x0, x1, x2) = x0 + x1 + x2 + 10,
         
         [a] = 0
        orientation:
         active(f(a(),X,X)) = 2X + 12 >= X + 16 = mark(f(X,b(),b()))
         
         active(b()) = 4 >= 2 = mark(a())
         
         active(f(X1,X2,X3)) = X1 + X2 + X3 + 12 >= X1 + X2 + X3 + 12 = f(X1,active(X2),X3)
         
         f(X1,mark(X2),X3) = X1 + X2 + X3 + 12 >= X1 + X2 + X3 + 12 = mark(f(X1,X2,X3))
         
         proper(f(X1,X2,X3)) = X1 + X2 + X3 + 12 >= X1 + X2 + X3 + 16 = f(proper(X1),proper(X2),proper(X3))
         
         top(mark(X)) = X + 4 >= X + 4 = top(proper(X))
         
         proper(a()) = 2 >= 2 = ok(a())
         
         proper(b()) = 4 >= 4 = ok(b())
         
         f(ok(X1),ok(X2),ok(X3)) = X1 + X2 + X3 + 16 >= X1 + X2 + X3 + 12 = ok(f(X1,X2,X3))
         
         top(ok(X)) = X + 4 >= X + 4 = top(active(X))
        problem:
         strict:
          active(f(a(),X,X)) -> mark(f(X,b(),b()))
          active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
          f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
          proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
         weak:
          active(b()) -> mark(a())
          top(mark(X)) -> top(proper(X))
          proper(a()) -> ok(a())
          proper(b()) -> ok(b())
          f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
          top(ok(X)) -> top(active(X))
        Splitting Processor:
         strict:
          active(f(a(),X,X)) -> mark(f(X,b(),b()))
         weak:
          active(b()) -> mark(a())
          top(mark(X)) -> top(proper(X))
          proper(a()) -> ok(a())
          proper(b()) -> ok(b())
          f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
          top(ok(X)) -> top(active(X))
          active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
          f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
          proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
         Matrix Interpretation Processor:
          dimension: 4
          max_matrix:
           [1 1 1 0]
           [0 0 1 0]
           [0 0 0 1]
           [0 0 0 0]
           interpretation:
                        [1 0 0 0]  
                        [0 0 1 0]  
            [top](x0) = [0 0 0 0]x0
                        [0 0 0 0]  ,
            
                       [1 1 0 0]  
                       [0 0 1 0]  
            [ok](x0) = [0 0 0 0]x0
                       [0 0 0 0]  ,
            
                           [1 0 0 0]  
                           [0 0 1 0]  
            [proper](x0) = [0 0 0 0]x0
                           [0 0 0 0]  ,
            
                         [1 0 0 0]  
                         [0 0 0 0]  
            [mark](x0) = [0 0 0 1]x0
                         [0 0 0 0]  ,
            
                  [0]
                  [0]
            [b] = [0]
                  [0],
            
                           [1 0 0 0]  
                           [0 0 0 0]  
            [active](x0) = [0 0 0 0]x0
                           [0 0 0 0]  ,
            
                              [1 1 1 0]     [1 0 0 0]     [1 1 1 0]  
                              [0 0 0 0]     [0 0 0 0]     [0 0 0 0]  
            [f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0 0 0 0]x2
                              [0 0 0 0]     [0 0 0 0]     [0 0 0 0]  ,
            
                  [0]
                  [0]
            [a] = [1]
                  [0]
           orientation:
                                 [2 1 1 0]    [1]    [1 1 1 0]                      
                                 [0 0 0 0]    [0]    [0 0 0 0]                      
            active(f(a(),X,X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X = mark(f(X,b(),b()))
                                 [0 0 0 0]    [0]    [0 0 0 0]                      
            
                          [0]    [0]            
                          [0]    [0]            
            active(b()) = [0] >= [0] = mark(a())
                          [0]    [0]            
            
                           [1 0 0 0]     [1 0 0 0]                  
                           [0 0 0 1]     [0 0 0 0]                  
            top(mark(X)) = [0 0 0 0]X >= [0 0 0 0]X = top(proper(X))
                           [0 0 0 0]     [0 0 0 0]                  
            
                          [0]    [0]          
                          [1]    [1]          
            proper(a()) = [0] >= [0] = ok(a())
                          [0]    [0]          
            
                          [0]    [0]          
                          [0]    [0]          
            proper(b()) = [0] >= [0] = ok(b())
                          [0]    [0]          
            
                                      [1 1 1 0]     [1 1 0 0]     [1 1 1 0]      [1 1 1 0]     [1 0 0 0]     [1 1 1 0]                    
                                      [0 0 0 0]     [0 0 0 0]     [0 0 0 0]      [0 0 0 0]     [0 0 0 0]     [0 0 0 0]                    
            f(ok(X1),ok(X2),ok(X3)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 = ok(f(X1,X2,X3))
                                      [0 0 0 0]     [0 0 0 0]     [0 0 0 0]      [0 0 0 0]     [0 0 0 0]     [0 0 0 0]                    
            
                         [1 1 0 0]     [1 0 0 0]                  
                         [0 0 0 0]     [0 0 0 0]                  
            top(ok(X)) = [0 0 0 0]X >= [0 0 0 0]X = top(active(X))
                         [0 0 0 0]     [0 0 0 0]                  
            
                                  [1 1 1 0]     [1 0 0 0]     [1 1 1 0]      [1 1 1 0]     [1 0 0 0]     [1 1 1 0]                        
                                  [0 0 0 0]     [0 0 0 0]     [0 0 0 0]      [0 0 0 0]     [0 0 0 0]     [0 0 0 0]                        
            active(f(X1,X2,X3)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 = f(X1,active(X2),X3)
                                  [0 0 0 0]     [0 0 0 0]     [0 0 0 0]      [0 0 0 0]     [0 0 0 0]     [0 0 0 0]                        
            
                                [1 1 1 0]     [1 0 0 0]     [1 1 1 0]      [1 1 1 0]     [1 0 0 0]     [1 1 1 0]                      
                                [0 0 0 0]     [0 0 0 0]     [0 0 0 0]      [0 0 0 0]     [0 0 0 0]     [0 0 0 0]                      
            f(X1,mark(X2),X3) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 = mark(f(X1,X2,X3))
                                [0 0 0 0]     [0 0 0 0]     [0 0 0 0]      [0 0 0 0]     [0 0 0 0]     [0 0 0 0]                      
            
                                  [1 1 1 0]     [1 0 0 0]     [1 1 1 0]      [1 0 1 0]     [1 0 0 0]     [1 0 1 0]                                        
                                  [0 0 0 0]     [0 0 0 0]     [0 0 0 0]      [0 0 0 0]     [0 0 0 0]     [0 0 0 0]                                        
            proper(f(X1,X2,X3)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 = f(proper(X1),proper(X2),proper(X3))
                                  [0 0 0 0]     [0 0 0 0]     [0 0 0 0]      [0 0 0 0]     [0 0 0 0]     [0 0 0 0]                                        
           problem:
            strict:
             
            weak:
             active(f(a(),X,X)) -> mark(f(X,b(),b()))
             active(b()) -> mark(a())
             top(mark(X)) -> top(proper(X))
             proper(a()) -> ok(a())
             proper(b()) -> ok(b())
             f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
             top(ok(X)) -> top(active(X))
             active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
             f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
             proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
           Qed
          
          strict:
           active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
           f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
           proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
          weak:
           active(f(a(),X,X)) -> mark(f(X,b(),b()))
           active(b()) -> mark(a())
           top(mark(X)) -> top(proper(X))
           proper(a()) -> ok(a())
           proper(b()) -> ok(b())
           f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
           top(ok(X)) -> top(active(X))
          Splitting Processor:
           strict:
            f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
           weak:
            active(f(a(),X,X)) -> mark(f(X,b(),b()))
            active(b()) -> mark(a())
            top(mark(X)) -> top(proper(X))
            proper(a()) -> ok(a())
            proper(b()) -> ok(b())
            f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
            top(ok(X)) -> top(active(X))
            active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
            proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
           Bounds Processor:
            bound: 0
            enrichment: match
            automaton:
             final states: {11,9,8,7,6,5}
             transitions:
              active0(2) -> 5*
              active0(9) -> 5*
              active0(4) -> 5*
              active0(11) -> 5*
              active0(1) -> 5*
              active0(3) -> 5*
              f0(3,4,2) -> 7*
              f0(3,2,11) -> 7*
              f0(3,4,11) -> 7*
              f0(11,1,4) -> 7*
              f0(1,1,4) -> 7*
              f0(11,3,4) -> 7*
              f0(1,3,4) -> 7*
              f0(11,2,9) -> 7*
              f0(1,2,9) -> 7*
              f0(11,4,9) -> 7*
              f0(11,9,4) -> 7*
              f0(1,4,9) -> 7*
              f0(1,9,4) -> 7*
              f0(11,11,4) -> 7*
              f0(11,1,1) -> 7*
              f0(9,1,2) -> 7*
              f0(4,1,2) -> 7*
              f0(1,11,4) -> 7*
              f0(1,1,1) -> 7*
              f0(11,3,1) -> 7*
              f0(9,3,2) -> 7*
              f0(4,3,2) -> 7*
              f0(1,3,1) -> 7*
              f0(9,1,11) -> 7*
              f0(4,1,11) -> 7*
              f0(9,3,11) -> 7*
              f0(4,3,11) -> 7*
              f0(11,9,1) -> 7*
              f0(9,9,2) -> 7*
              f0(4,9,2) -> 7*
              f0(1,9,1) -> 7*
              f0(11,11,1) -> 7*
              f0(9,11,2) -> 7*
              f0(4,11,2) -> 7*
              f0(1,11,1) -> 7*
              f0(2,2,4) -> 7*
              f0(9,9,11) -> 7*
              f0(4,9,11) -> 7*
              f0(2,4,4) -> 7*
              f0(9,11,11) -> 7*
              f0(11,2,3) -> 7*
              f0(4,11,11) -> 7*
              f0(2,1,9) -> 7*
              f0(1,2,3) -> 7*
              f0(11,4,3) -> 7*
              f0(2,3,9) -> 7*
              f0(1,4,3) -> 7*
              f0(2,2,1) -> 7*
              f0(2,9,9) -> 7*
              f0(2,4,1) -> 7*
              f0(2,11,9) -> 7*
              f0(3,1,4) -> 7*
              f0(3,3,4) -> 7*
              f0(2,1,3) -> 7*
              f0(3,2,9) -> 7*
              f0(2,3,3) -> 7*
              f0(3,4,9) -> 7*
              f0(3,9,4) -> 7*
              f0(11,1,2) -> 7*
              f0(3,11,4) -> 7*
              f0(3,1,1) -> 7*
              f0(1,1,2) -> 7*
              f0(11,3,2) -> 7*
              f0(3,3,1) -> 7*
              f0(1,3,2) -> 7*
              f0(11,1,11) -> 7*
              f0(2,9,3) -> 7*
              f0(11,3,11) -> 7*
              f0(1,1,11) -> 7*
              f0(2,11,3) -> 7*
              f0(11,9,2) -> 7*
              f0(1,3,11) -> 7*
              f0(3,9,1) -> 7*
              f0(1,9,2) -> 7*
              f0(11,11,2) -> 7*
              f0(9,2,4) -> 7*
              f0(3,11,1) -> 7*
              f0(1,11,2) -> 7*
              f0(4,2,4) -> 7*
              f0(11,9,11) -> 7*
              f0(9,4,4) -> 7*
              f0(4,4,4) -> 7*
              f0(11,11,11) -> 7*
              f0(1,9,11) -> 7*
              f0(9,1,9) -> 7*
              f0(4,1,9) -> 7*
              f0(1,11,11) -> 7*
              f0(9,3,9) -> 7*
              f0(3,2,3) -> 7*
              f0(4,3,9) -> 7*
              f0(3,4,3) -> 7*
              f0(9,2,1) -> 7*
              f0(4,2,1) -> 7*
              f0(2,2,2) -> 7*
              f0(9,9,9) -> 7*
              f0(9,4,1) -> 7*
              f0(4,9,9) -> 7*
              f0(4,4,1) -> 7*
              f0(2,4,2) -> 7*
              f0(9,11,9) -> 7*
              f0(4,11,9) -> 7*
              f0(2,2,11) -> 7*
              f0(2,4,11) -> 7*
              f0(9,1,3) -> 7*
              f0(4,1,3) -> 7*
              f0(9,3,3) -> 7*
              f0(4,3,3) -> 7*
              f0(3,1,2) -> 7*
              f0(9,9,3) -> 7*
              f0(3,3,2) -> 7*
              f0(4,9,3) -> 7*
              f0(9,11,3) -> 7*
              f0(3,1,11) -> 7*
              f0(4,11,3) -> 7*
              f0(3,3,11) -> 7*
              f0(3,9,2) -> 7*
              f0(11,2,4) -> 7*
              f0(3,11,2) -> 7*
              f0(1,2,4) -> 7*
              f0(11,4,4) -> 7*
              f0(3,9,11) -> 7*
              f0(11,1,9) -> 7*
              f0(1,4,4) -> 7*
              f0(3,11,11) -> 7*
              f0(1,1,9) -> 7*
              f0(11,3,9) -> 7*
              f0(1,3,9) -> 7*
              f0(11,2,1) -> 7*
              f0(9,2,2) -> 7*
              f0(4,2,2) -> 7*
              f0(11,9,9) -> 7*
              f0(1,2,1) -> 7*
              f0(11,4,1) -> 7*
              f0(9,4,2) -> 7*
              f0(4,4,2) -> 7*
              f0(1,9,9) -> 7*
              f0(11,11,9) -> 7*
              f0(1,4,1) -> 7*
              f0(9,2,11) -> 7*
              f0(1,11,9) -> 7*
              f0(4,2,11) -> 7*
              f0(9,4,11) -> 7*
              f0(4,4,11) -> 7*
              f0(2,1,4) -> 7*
              f0(2,3,4) -> 7*
              f0(11,1,3) -> 7*
              f0(1,1,3) -> 7*
              f0(11,3,3) -> 7*
              f0(2,2,9) -> 7*
              f0(1,3,3) -> 7*
              f0(2,4,9) -> 7*
              f0(2,9,4) -> 7*
              f0(2,11,4) -> 7*
              f0(2,1,1) -> 7*
              f0(11,9,3) -> 7*
              f0(2,3,1) -> 7*
              f0(1,9,3) -> 7*
              f0(11,11,3) -> 7*
              f0(1,11,3) -> 7*
              f0(2,9,1) -> 7*
              f0(2,11,1) -> 7*
              f0(3,2,4) -> 7*
              f0(3,4,4) -> 7*
              f0(3,1,9) -> 7*
              f0(2,2,3) -> 7*
              f0(3,3,9) -> 7*
              f0(2,4,3) -> 7*
              f0(11,2,2) -> 7*
              f0(3,2,1) -> 7*
              f0(1,2,2) -> 7*
              f0(11,4,2) -> 7*
              f0(3,9,9) -> 7*
              f0(3,4,1) -> 7*
              f0(1,4,2) -> 7*
              f0(11,2,11) -> 7*
              f0(3,11,9) -> 7*
              f0(1,2,11) -> 7*
              f0(11,4,11) -> 7*
              f0(1,4,11) -> 7*
              f0(9,1,4) -> 7*
              f0(4,1,4) -> 7*
              f0(9,3,4) -> 7*
              f0(4,3,4) -> 7*
              f0(9,2,9) -> 7*
              f0(3,1,3) -> 7*
              f0(4,2,9) -> 7*
              f0(9,4,9) -> 7*
              f0(9,9,4) -> 7*
              f0(3,3,3) -> 7*
              f0(4,4,9) -> 7*
              f0(4,9,4) -> 7*
              f0(9,11,4) -> 7*
              f0(9,1,1) -> 7*
              f0(4,11,4) -> 7*
              f0(4,1,1) -> 7*
              f0(2,1,2) -> 7*
              f0(9,3,1) -> 7*
              f0(4,3,1) -> 7*
              f0(2,3,2) -> 7*
              f0(3,9,3) -> 7*
              f0(2,1,11) -> 7*
              f0(3,11,3) -> 7*
              f0(2,3,11) -> 7*
              f0(9,9,1) -> 7*
              f0(4,9,1) -> 7*
              f0(2,9,2) -> 7*
              f0(9,11,1) -> 7*
              f0(4,11,1) -> 7*
              f0(2,11,2) -> 7*
              f0(2,9,11) -> 7*
              f0(9,2,3) -> 7*
              f0(2,11,11) -> 7*
              f0(4,2,3) -> 7*
              f0(9,4,3) -> 7*
              f0(4,4,3) -> 7*
              f0(3,2,2) -> 7*
              proper0(2) -> 6*
              proper0(9) -> 6*
              proper0(4) -> 6*
              proper0(11) -> 6*
              proper0(1) -> 6*
              proper0(3) -> 6*
              mark0(7) -> 7*
              mark0(2) -> 9*,5,1
              mark0(9) -> 1*
              mark0(4) -> 1*
              mark0(11) -> 1*
              mark0(1) -> 1*
              mark0(3) -> 1*
              a0() -> 2*
              b0() -> 3*
              top0(5) -> 8*
              top0(2) -> 8*
              top0(9) -> 8*
              top0(4) -> 8*
              top0(11) -> 8*
              top0(6) -> 8*
              top0(1) -> 8*
              top0(3) -> 8*
              ok0(7) -> 7*
              ok0(2) -> 11*,6,4
              ok0(9) -> 4*
              ok0(4) -> 4*
              ok0(11) -> 4*
              ok0(1) -> 4*
              ok0(3) -> 11*,6,4
            problem:
             strict:
              proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
             weak:
              active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
              f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
              active(f(a(),X,X)) -> mark(f(X,b(),b()))
              active(b()) -> mark(a())
              top(mark(X)) -> top(proper(X))
              proper(a()) -> ok(a())
              proper(b()) -> ok(b())
              f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
              top(ok(X)) -> top(active(X))
            Bounds Processor:
             bound: 0
             enrichment: match
             automaton:
              final states: {11,9,8,7,6,5}
              transitions:
               active0(2) -> 6*
               active0(9) -> 6*
               active0(4) -> 6*
               active0(11) -> 6*
               active0(1) -> 6*
               active0(3) -> 6*
               f0(3,4,2) -> 7*
               f0(3,2,11) -> 7*
               f0(3,4,11) -> 7*
               f0(11,1,4) -> 7*
               f0(1,1,4) -> 7*
               f0(11,3,4) -> 7*
               f0(1,3,4) -> 7*
               f0(11,2,9) -> 7*
               f0(1,2,9) -> 7*
               f0(11,4,9) -> 7*
               f0(11,9,4) -> 7*
               f0(1,4,9) -> 7*
               f0(1,9,4) -> 7*
               f0(11,11,4) -> 7*
               f0(11,1,1) -> 7*
               f0(9,1,2) -> 7*
               f0(4,1,2) -> 7*
               f0(1,11,4) -> 7*
               f0(1,1,1) -> 7*
               f0(11,3,1) -> 7*
               f0(9,3,2) -> 7*
               f0(4,3,2) -> 7*
               f0(1,3,1) -> 7*
               f0(9,1,11) -> 7*
               f0(4,1,11) -> 7*
               f0(9,3,11) -> 7*
               f0(4,3,11) -> 7*
               f0(11,9,1) -> 7*
               f0(9,9,2) -> 7*
               f0(4,9,2) -> 7*
               f0(1,9,1) -> 7*
               f0(11,11,1) -> 7*
               f0(9,11,2) -> 7*
               f0(4,11,2) -> 7*
               f0(1,11,1) -> 7*
               f0(2,2,4) -> 7*
               f0(9,9,11) -> 7*
               f0(4,9,11) -> 7*
               f0(2,4,4) -> 7*
               f0(9,11,11) -> 7*
               f0(11,2,3) -> 7*
               f0(4,11,11) -> 7*
               f0(2,1,9) -> 7*
               f0(1,2,3) -> 7*
               f0(11,4,3) -> 7*
               f0(2,3,9) -> 7*
               f0(1,4,3) -> 7*
               f0(2,2,1) -> 7*
               f0(2,9,9) -> 7*
               f0(2,4,1) -> 7*
               f0(2,11,9) -> 7*
               f0(3,1,4) -> 7*
               f0(3,3,4) -> 7*
               f0(2,1,3) -> 7*
               f0(3,2,9) -> 7*
               f0(2,3,3) -> 7*
               f0(3,4,9) -> 7*
               f0(3,9,4) -> 7*
               f0(11,1,2) -> 7*
               f0(3,11,4) -> 7*
               f0(3,1,1) -> 7*
               f0(1,1,2) -> 7*
               f0(11,3,2) -> 7*
               f0(3,3,1) -> 7*
               f0(1,3,2) -> 7*
               f0(11,1,11) -> 7*
               f0(2,9,3) -> 7*
               f0(11,3,11) -> 7*
               f0(1,1,11) -> 7*
               f0(2,11,3) -> 7*
               f0(11,9,2) -> 7*
               f0(1,3,11) -> 7*
               f0(3,9,1) -> 7*
               f0(1,9,2) -> 7*
               f0(11,11,2) -> 7*
               f0(9,2,4) -> 7*
               f0(3,11,1) -> 7*
               f0(1,11,2) -> 7*
               f0(4,2,4) -> 7*
               f0(11,9,11) -> 7*
               f0(9,4,4) -> 7*
               f0(4,4,4) -> 7*
               f0(11,11,11) -> 7*
               f0(1,9,11) -> 7*
               f0(9,1,9) -> 7*
               f0(4,1,9) -> 7*
               f0(1,11,11) -> 7*
               f0(9,3,9) -> 7*
               f0(3,2,3) -> 7*
               f0(4,3,9) -> 7*
               f0(3,4,3) -> 7*
               f0(9,2,1) -> 7*
               f0(4,2,1) -> 7*
               f0(2,2,2) -> 7*
               f0(9,9,9) -> 7*
               f0(9,4,1) -> 7*
               f0(4,9,9) -> 7*
               f0(4,4,1) -> 7*
               f0(2,4,2) -> 7*
               f0(9,11,9) -> 7*
               f0(4,11,9) -> 7*
               f0(2,2,11) -> 7*
               f0(2,4,11) -> 7*
               f0(9,1,3) -> 7*
               f0(4,1,3) -> 7*
               f0(9,3,3) -> 7*
               f0(4,3,3) -> 7*
               f0(3,1,2) -> 7*
               f0(9,9,3) -> 7*
               f0(3,3,2) -> 7*
               f0(4,9,3) -> 7*
               f0(9,11,3) -> 7*
               f0(3,1,11) -> 7*
               f0(4,11,3) -> 7*
               f0(3,3,11) -> 7*
               f0(3,9,2) -> 7*
               f0(11,2,4) -> 7*
               f0(3,11,2) -> 7*
               f0(1,2,4) -> 7*
               f0(11,4,4) -> 7*
               f0(3,9,11) -> 7*
               f0(11,1,9) -> 7*
               f0(1,4,4) -> 7*
               f0(3,11,11) -> 7*
               f0(1,1,9) -> 7*
               f0(11,3,9) -> 7*
               f0(1,3,9) -> 7*
               f0(11,2,1) -> 7*
               f0(9,2,2) -> 7*
               f0(4,2,2) -> 7*
               f0(11,9,9) -> 7*
               f0(1,2,1) -> 7*
               f0(11,4,1) -> 7*
               f0(9,4,2) -> 7*
               f0(4,4,2) -> 7*
               f0(1,9,9) -> 7*
               f0(11,11,9) -> 7*
               f0(1,4,1) -> 7*
               f0(9,2,11) -> 7*
               f0(1,11,9) -> 7*
               f0(4,2,11) -> 7*
               f0(9,4,11) -> 7*
               f0(4,4,11) -> 7*
               f0(2,1,4) -> 7*
               f0(2,3,4) -> 7*
               f0(11,1,3) -> 7*
               f0(1,1,3) -> 7*
               f0(11,3,3) -> 7*
               f0(2,2,9) -> 7*
               f0(1,3,3) -> 7*
               f0(2,4,9) -> 7*
               f0(2,9,4) -> 7*
               f0(2,11,4) -> 7*
               f0(2,1,1) -> 7*
               f0(11,9,3) -> 7*
               f0(2,3,1) -> 7*
               f0(1,9,3) -> 7*
               f0(11,11,3) -> 7*
               f0(1,11,3) -> 7*
               f0(2,9,1) -> 7*
               f0(2,11,1) -> 7*
               f0(3,2,4) -> 7*
               f0(3,4,4) -> 7*
               f0(3,1,9) -> 7*
               f0(2,2,3) -> 7*
               f0(3,3,9) -> 7*
               f0(2,4,3) -> 7*
               f0(11,2,2) -> 7*
               f0(3,2,1) -> 7*
               f0(1,2,2) -> 7*
               f0(11,4,2) -> 7*
               f0(3,9,9) -> 7*
               f0(3,4,1) -> 7*
               f0(1,4,2) -> 7*
               f0(11,2,11) -> 7*
               f0(3,11,9) -> 7*
               f0(1,2,11) -> 7*
               f0(11,4,11) -> 7*
               f0(1,4,11) -> 7*
               f0(9,1,4) -> 7*
               f0(4,1,4) -> 7*
               f0(9,3,4) -> 7*
               f0(4,3,4) -> 7*
               f0(9,2,9) -> 7*
               f0(3,1,3) -> 7*
               f0(4,2,9) -> 7*
               f0(9,4,9) -> 7*
               f0(9,9,4) -> 7*
               f0(3,3,3) -> 7*
               f0(4,4,9) -> 7*
               f0(4,9,4) -> 7*
               f0(9,11,4) -> 7*
               f0(9,1,1) -> 7*
               f0(4,11,4) -> 7*
               f0(4,1,1) -> 7*
               f0(2,1,2) -> 7*
               f0(9,3,1) -> 7*
               f0(4,3,1) -> 7*
               f0(2,3,2) -> 7*
               f0(3,9,3) -> 7*
               f0(2,1,11) -> 7*
               f0(3,11,3) -> 7*
               f0(2,3,11) -> 7*
               f0(9,9,1) -> 7*
               f0(4,9,1) -> 7*
               f0(2,9,2) -> 7*
               f0(9,11,1) -> 7*
               f0(4,11,1) -> 7*
               f0(2,11,2) -> 7*
               f0(2,9,11) -> 7*
               f0(9,2,3) -> 7*
               f0(2,11,11) -> 7*
               f0(4,2,3) -> 7*
               f0(9,4,3) -> 7*
               f0(4,4,3) -> 7*
               f0(3,2,2) -> 7*
               proper0(2) -> 5*
               proper0(9) -> 5*
               proper0(4) -> 5*
               proper0(11) -> 5*
               proper0(1) -> 5*
               proper0(3) -> 5*
               mark0(7) -> 7*
               mark0(2) -> 9*,6,1
               mark0(9) -> 1*
               mark0(4) -> 1*
               mark0(11) -> 1*
               mark0(1) -> 1*
               mark0(3) -> 1*
               a0() -> 2*
               b0() -> 3*
               top0(5) -> 8*
               top0(2) -> 8*
               top0(9) -> 8*
               top0(4) -> 8*
               top0(11) -> 8*
               top0(6) -> 8*
               top0(1) -> 8*
               top0(3) -> 8*
               ok0(7) -> 7*
               ok0(2) -> 11*,5,4
               ok0(9) -> 4*
               ok0(4) -> 4*
               ok0(11) -> 4*
               ok0(1) -> 4*
               ok0(3) -> 11*,5,4
             problem:
              strict:
               
              weak:
               proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
               active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
               f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
               active(f(a(),X,X)) -> mark(f(X,b(),b()))
               active(b()) -> mark(a())
               top(mark(X)) -> top(proper(X))
               proper(a()) -> ok(a())
               proper(b()) -> ok(b())
               f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
               top(ok(X)) -> top(active(X))
             Qed
           
           strict:
            active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
            proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
           weak:
            f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
            active(f(a(),X,X)) -> mark(f(X,b(),b()))
            active(b()) -> mark(a())
            top(mark(X)) -> top(proper(X))
            proper(a()) -> ok(a())
            proper(b()) -> ok(b())
            f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
            top(ok(X)) -> top(active(X))
           Bounds Processor:
            bound: 1
            enrichment: match
            automaton:
             final states: {16,14,12,8,7,6,5}
             transitions:
              active0(2) -> 6*
              active0(14) -> 6*
              active0(4) -> 6*
              active0(16) -> 6*
              active0(1) -> 6*
              active0(3) -> 6*
              f0(3,4,2) -> 5*
              f0(16,3,16) -> 5*
              f0(14,14,3) -> 5*
              f0(1,3,16) -> 5*
              f0(16,1,4) -> 5*
              f0(3,14,14) -> 5*
              f0(14,16,3) -> 5*
              f0(4,14,3) -> 5*
              f0(3,1,16) -> 5*
              f0(16,3,4) -> 5*
              f0(3,16,14) -> 5*
              f0(4,16,3) -> 5*
              f0(1,1,4) -> 5*
              f0(14,1,14) -> 5*
              f0(1,3,4) -> 5*
              f0(3,14,2) -> 5*
              f0(14,3,14) -> 5*
              f0(4,1,14) -> 5*
              f0(3,16,2) -> 5*
              f0(4,3,14) -> 5*
              f0(16,1,1) -> 5*
              f0(14,1,2) -> 5*
              f0(16,3,1) -> 5*
              f0(14,3,2) -> 5*
              f0(4,1,2) -> 5*
              f0(1,1,1) -> 5*
              f0(4,3,2) -> 5*
              f0(1,3,1) -> 5*
              f0(2,2,16) -> 5*
              f0(2,4,16) -> 5*
              f0(2,2,4) -> 5*
              f0(2,4,4) -> 5*
              f0(16,2,3) -> 5*
              f0(16,4,3) -> 5*
              f0(1,2,3) -> 5*
              f0(2,14,16) -> 5*
              f0(1,4,3) -> 5*
              f0(2,16,16) -> 5*
              f0(2,2,1) -> 5*
              f0(2,14,4) -> 5*
              f0(2,4,1) -> 5*
              f0(2,16,4) -> 5*
              f0(16,14,3) -> 5*
              f0(3,3,16) -> 5*
              f0(16,16,3) -> 5*
              f0(1,14,3) -> 5*
              f0(3,1,4) -> 5*
              f0(1,16,3) -> 5*
              f0(16,1,14) -> 5*
              f0(3,3,4) -> 5*
              f0(2,14,1) -> 5*
              f0(16,3,14) -> 5*
              f0(1,1,14) -> 5*
              f0(2,1,3) -> 5*
              f0(2,16,1) -> 5*
              f0(1,3,14) -> 5*
              f0(2,3,3) -> 5*
              f0(16,1,2) -> 5*
              f0(16,3,2) -> 5*
              f0(3,1,1) -> 5*
              f0(1,1,2) -> 5*
              f0(3,3,1) -> 5*
              f0(1,3,2) -> 5*
              f0(14,2,16) -> 5*
              f0(4,2,16) -> 5*
              f0(14,4,16) -> 5*
              f0(4,4,16) -> 5*
              f0(14,2,4) -> 5*
              f0(14,4,4) -> 5*
              f0(4,2,4) -> 5*
              f0(4,4,4) -> 5*
              f0(14,14,16) -> 5*
              f0(2,2,14) -> 5*
              f0(3,2,3) -> 5*
              f0(14,16,16) -> 5*
              f0(4,14,16) -> 5*
              f0(2,4,14) -> 5*
              f0(3,4,3) -> 5*
              f0(14,2,1) -> 5*
              f0(4,16,16) -> 5*
              f0(14,14,4) -> 5*
              f0(14,4,1) -> 5*
              f0(4,2,1) -> 5*
              f0(2,2,2) -> 5*
              f0(14,16,4) -> 5*
              f0(4,14,4) -> 5*
              f0(4,4,1) -> 5*
              f0(2,4,2) -> 5*
              f0(4,16,4) -> 5*
              f0(2,14,14) -> 5*
              f0(3,14,3) -> 5*
              f0(2,1,16) -> 5*
              f0(2,16,14) -> 5*
              f0(3,16,3) -> 5*
              f0(14,14,1) -> 5*
              f0(14,1,3) -> 5*
              f0(14,16,1) -> 5*
              f0(4,14,1) -> 5*
              f0(2,14,2) -> 5*
              f0(3,1,14) -> 5*
              f0(14,3,3) -> 5*
              f0(4,1,3) -> 5*
              f0(4,16,1) -> 5*
              f0(2,16,2) -> 5*
              f0(3,3,14) -> 5*
              f0(4,3,3) -> 5*
              f0(3,1,2) -> 5*
              f0(3,3,2) -> 5*
              f0(16,2,16) -> 5*
              f0(16,4,16) -> 5*
              f0(1,2,16) -> 5*
              f0(1,4,16) -> 5*
              f0(16,2,4) -> 5*
              f0(16,4,4) -> 5*
              f0(1,2,4) -> 5*
              f0(14,2,14) -> 5*
              f0(1,4,4) -> 5*
              f0(16,14,16) -> 5*
              f0(4,2,14) -> 5*
              f0(14,4,14) -> 5*
              f0(16,16,16) -> 5*
              f0(4,4,14) -> 5*
              f0(1,14,16) -> 5*
              f0(16,2,1) -> 5*
              f0(14,2,2) -> 5*
              f0(1,16,16) -> 5*
              f0(16,14,4) -> 5*
              f0(16,4,1) -> 5*
              f0(14,4,2) -> 5*
              f0(4,2,2) -> 5*
              f0(1,2,1) -> 5*
              f0(16,16,4) -> 5*
              f0(4,4,2) -> 5*
              f0(1,14,4) -> 5*
              f0(1,4,1) -> 5*
              f0(14,14,14) -> 5*
              f0(1,16,4) -> 5*
              f0(2,3,16) -> 5*
              f0(14,16,14) -> 5*
              f0(4,14,14) -> 5*
              f0(4,16,14) -> 5*
              f0(2,1,4) -> 5*
              f0(16,14,1) -> 5*
              f0(14,14,2) -> 5*
              f0(2,3,4) -> 5*
              f0(16,1,3) -> 5*
              f0(16,16,1) -> 5*
              f0(14,16,2) -> 5*
              f0(4,14,2) -> 5*
              f0(1,14,1) -> 5*
              f0(16,3,3) -> 5*
              f0(4,16,2) -> 5*
              f0(1,1,3) -> 5*
              f0(1,16,1) -> 5*
              f0(1,3,3) -> 5*
              f0(2,1,1) -> 5*
              f0(2,3,1) -> 5*
              f0(3,2,16) -> 5*
              f0(3,4,16) -> 5*
              f0(3,2,4) -> 5*
              f0(16,2,14) -> 5*
              f0(3,4,4) -> 5*
              f0(16,4,14) -> 5*
              f0(1,2,14) -> 5*
              f0(2,2,3) -> 5*
              f0(3,14,16) -> 5*
              f0(1,4,14) -> 5*
              f0(2,4,3) -> 5*
              f0(16,2,2) -> 5*
              f0(3,16,16) -> 5*
              f0(16,4,2) -> 5*
              f0(3,2,1) -> 5*
              f0(1,2,2) -> 5*
              f0(14,1,16) -> 5*
              f0(3,14,4) -> 5*
              f0(3,4,1) -> 5*
              f0(1,4,2) -> 5*
              f0(14,3,16) -> 5*
              f0(4,1,16) -> 5*
              f0(16,14,14) -> 5*
              f0(3,16,4) -> 5*
              f0(4,3,16) -> 5*
              f0(16,16,14) -> 5*
              f0(14,1,4) -> 5*
              f0(1,14,14) -> 5*
              f0(2,14,3) -> 5*
              f0(1,1,16) -> 5*
              f0(1,16,14) -> 5*
              f0(14,3,4) -> 5*
              f0(4,1,4) -> 5*
              f0(2,16,3) -> 5*
              f0(16,14,2) -> 5*
              f0(4,3,4) -> 5*
              f0(16,16,2) -> 5*
              f0(3,14,1) -> 5*
              f0(1,14,2) -> 5*
              f0(2,1,14) -> 5*
              f0(3,1,3) -> 5*
              f0(3,16,1) -> 5*
              f0(1,16,2) -> 5*
              f0(2,3,14) -> 5*
              f0(3,3,3) -> 5*
              f0(14,1,1) -> 5*
              f0(14,3,1) -> 5*
              f0(4,1,1) -> 5*
              f0(2,1,2) -> 5*
              f0(4,3,1) -> 5*
              f0(2,3,2) -> 5*
              f0(14,2,3) -> 5*
              f0(3,2,14) -> 5*
              f0(14,4,3) -> 5*
              f0(4,2,3) -> 5*
              f0(3,4,14) -> 5*
              f0(4,4,3) -> 5*
              f0(3,2,2) -> 5*
              f0(16,1,16) -> 5*
              proper0(2) -> 8*
              proper0(14) -> 8*
              proper0(4) -> 8*
              proper0(16) -> 8*
              proper0(1) -> 8*
              proper0(3) -> 8*
              mark0(2) -> 14*,6,1
              mark0(14) -> 1*
              mark0(4) -> 1*
              mark0(16) -> 1*
              mark0(1) -> 1*
              mark0(3) -> 1*
              a0() -> 2*
              b0() -> 3*
              top0(2) -> 7*
              top0(14) -> 7*
              top0(4) -> 7*
              top0(16) -> 7*
              top0(6) -> 7*
              top0(1) -> 7*
              top0(8) -> 7*
              top0(3) -> 7*
              ok0(5) -> 5*
              ok0(12) -> 5*
              ok0(2) -> 16*,8,4
              ok0(14) -> 4*
              ok0(4) -> 4*
              ok0(16) -> 4*
              ok0(1) -> 4*
              ok0(3) -> 16*,8,4
              mark1(10) -> 5*
              mark1(5) -> 12*
              mark1(12) -> 12*,5
              f1(3,2,2) -> 12*,5,10
              f1(16,1,16) -> 5,12*
              f1(3,4,2) -> 12*,5,10
              f1(16,3,16) -> 5,12*
              f1(14,14,3) -> 5,12*
              f1(1,3,16) -> 5,12*
              f1(16,1,4) -> 5,12*
              f1(3,14,14) -> 5,12*
              f1(14,16,3) -> 5,12*
              f1(4,14,3) -> 5,12*
              f1(3,1,16) -> 5,12*
              f1(16,3,4) -> 5,12*
              f1(3,16,14) -> 5,12*
              f1(4,16,3) -> 5,12*
              f1(1,1,4) -> 12*,5,10
              f1(14,1,14) -> 5,12*
              f1(1,3,4) -> 12*,5,10
              f1(3,14,2) -> 5,12*
              f1(14,3,14) -> 5,12*
              f1(4,1,14) -> 5,12*
              f1(3,16,2) -> 5,12*
              f1(4,3,14) -> 5,12*
              f1(16,1,1) -> 5,12*
              f1(14,1,2) -> 5,12*
              f1(16,3,1) -> 5,12*
              f1(14,3,2) -> 5,12*
              f1(4,1,2) -> 12*,5,10
              f1(1,1,1) -> 12*,5,10
              f1(4,3,2) -> 12*,5,10
              f1(1,3,1) -> 12*,5,10
              f1(2,2,16) -> 5,12*
              f1(2,4,16) -> 5,12*
              f1(2,2,4) -> 12*,5,10
              f1(2,4,4) -> 12*,5,10
              f1(16,2,3) -> 5,12*
              f1(16,4,3) -> 5,12*
              f1(1,2,3) -> 12*,5,10
              f1(2,14,16) -> 5,12*
              f1(1,4,3) -> 12*,5,10
              f1(2,16,16) -> 5,12*
              f1(2,2,1) -> 12*,5,10
              f1(2,14,4) -> 5,12*
              f1(2,4,1) -> 12*,5,10
              f1(2,16,4) -> 5,12*
              f1(16,14,3) -> 5,12*
              f1(3,3,16) -> 5,12*
              f1(16,16,3) -> 5,12*
              f1(1,14,3) -> 5,12*
              f1(3,1,4) -> 12*,5,10
              f1(1,16,3) -> 5,12*
              f1(16,1,14) -> 5,12*
              f1(3,3,4) -> 12*,5,10
              f1(2,14,1) -> 5,12*
              f1(16,3,14) -> 5,12*
              f1(1,1,14) -> 5,12*
              f1(2,1,3) -> 12*,5,10
              f1(2,16,1) -> 5,12*
              f1(1,3,14) -> 5,12*
              f1(2,3,3) -> 12*,5,10
              f1(16,1,2) -> 5,12*
              f1(16,3,2) -> 5,12*
              f1(3,1,1) -> 12*,5,10
              f1(1,1,2) -> 12*,5,10
              f1(3,3,1) -> 12*,5,10
              f1(1,3,2) -> 12*,5,10
              f1(14,2,16) -> 5,12*
              f1(4,2,16) -> 5,12*
              f1(14,4,16) -> 5,12*
              f1(4,4,16) -> 5,12*
              f1(14,2,4) -> 5,12*
              f1(14,4,4) -> 5,12*
              f1(4,2,4) -> 12*,5,10
              f1(4,4,4) -> 12*,5,10
              f1(14,14,16) -> 5,12*
              f1(2,2,14) -> 5,12*
              f1(3,2,3) -> 12*,5,10
              f1(14,16,16) -> 5,12*
              f1(4,14,16) -> 5,12*
              f1(2,4,14) -> 5,12*
              f1(3,4,3) -> 12*,5,10
              f1(14,2,1) -> 5,12*
              f1(4,16,16) -> 5,12*
              f1(14,14,4) -> 5,12*
              f1(14,4,1) -> 5,12*
              f1(4,2,1) -> 12*,5,10
              f1(2,2,2) -> 12*,5,10
              f1(14,16,4) -> 5,12*
              f1(4,14,4) -> 5,12*
              f1(4,4,1) -> 12*,5,10
              f1(2,4,2) -> 12*,5,10
              f1(4,16,4) -> 5,12*
              f1(2,14,14) -> 5,12*
              f1(3,14,3) -> 5,12*
              f1(2,1,16) -> 5,12*
              f1(2,16,14) -> 5,12*
              f1(3,16,3) -> 5,12*
              f1(14,14,1) -> 5,12*
              f1(14,1,3) -> 5,12*
              f1(14,16,1) -> 5,12*
              f1(4,14,1) -> 5,12*
              f1(2,14,2) -> 5,12*
              f1(3,1,14) -> 5,12*
              f1(14,3,3) -> 5,12*
              f1(4,1,3) -> 12*,5,10
              f1(4,16,1) -> 5,12*
              f1(2,16,2) -> 5,12*
              f1(3,3,14) -> 5,12*
              f1(4,3,3) -> 12*,5,10
              f1(3,1,2) -> 12*,5,10
              f1(3,3,2) -> 12*,5,10
              f1(16,2,16) -> 5,12*
              f1(16,4,16) -> 5,12*
              f1(1,2,16) -> 5,12*
              f1(1,4,16) -> 5,12*
              f1(16,2,4) -> 5,12*
              f1(16,4,4) -> 5,12*
              f1(1,2,4) -> 12*,5,10
              f1(14,2,14) -> 5,12*
              f1(1,4,4) -> 12*,5,10
              f1(16,14,16) -> 5,12*
              f1(4,2,14) -> 5,12*
              f1(14,4,14) -> 5,12*
              f1(16,16,16) -> 5,12*
              f1(4,4,14) -> 5,12*
              f1(1,14,16) -> 5,12*
              f1(16,2,1) -> 5,12*
              f1(14,2,2) -> 5,12*
              f1(1,16,16) -> 5,12*
              f1(16,14,4) -> 5,12*
              f1(16,4,1) -> 5,12*
              f1(14,4,2) -> 5,12*
              f1(4,2,2) -> 12*,5,10
              f1(1,2,1) -> 12*,5,10
              f1(16,16,4) -> 5,12*
              f1(4,4,2) -> 12*,5,10
              f1(1,14,4) -> 5,12*
              f1(1,4,1) -> 12*,5,10
              f1(14,14,14) -> 5,12*
              f1(1,16,4) -> 5,12*
              f1(2,3,16) -> 5,12*
              f1(14,16,14) -> 5,12*
              f1(4,14,14) -> 5,12*
              f1(4,16,14) -> 5,12*
              f1(2,1,4) -> 12*,5,10
              f1(16,14,1) -> 5,12*
              f1(14,14,2) -> 5,12*
              f1(2,3,4) -> 12*,5,10
              f1(16,1,3) -> 5,12*
              f1(16,16,1) -> 5,12*
              f1(14,16,2) -> 5,12*
              f1(4,14,2) -> 5,12*
              f1(1,14,1) -> 5,12*
              f1(16,3,3) -> 5,12*
              f1(4,16,2) -> 5,12*
              f1(1,1,3) -> 12*,5,10
              f1(1,16,1) -> 5,12*
              f1(1,3,3) -> 12*,5,10
              f1(2,1,1) -> 12*,5,10
              f1(2,3,1) -> 12*,5,10
              f1(3,2,16) -> 5,12*
              f1(3,4,16) -> 5,12*
              f1(3,2,4) -> 12*,5,10
              f1(16,2,14) -> 5,12*
              f1(3,4,4) -> 12*,5,10
              f1(16,4,14) -> 5,12*
              f1(1,2,14) -> 5,12*
              f1(2,2,3) -> 12*,5,10
              f1(3,14,16) -> 5,12*
              f1(1,4,14) -> 5,12*
              f1(2,4,3) -> 12*,5,10
              f1(16,2,2) -> 5,12*
              f1(3,16,16) -> 5,12*
              f1(16,4,2) -> 5,12*
              f1(3,2,1) -> 12*,5,10
              f1(1,2,2) -> 12*,5,10
              f1(14,1,16) -> 5,12*
              f1(3,14,4) -> 5,12*
              f1(3,4,1) -> 12*,5,10
              f1(1,4,2) -> 12*,5,10
              f1(14,3,16) -> 5,12*
              f1(4,1,16) -> 5,12*
              f1(16,14,14) -> 5,12*
              f1(3,16,4) -> 5,12*
              f1(4,3,16) -> 5,12*
              f1(16,16,14) -> 5,12*
              f1(14,1,4) -> 5,12*
              f1(1,14,14) -> 5,12*
              f1(2,14,3) -> 5,12*
              f1(1,1,16) -> 5,12*
              f1(1,16,14) -> 5,12*
              f1(14,3,4) -> 5,12*
              f1(4,1,4) -> 12*,5,10
              f1(2,16,3) -> 5,12*
              f1(16,14,2) -> 5,12*
              f1(4,3,4) -> 12*,5,10
              f1(16,16,2) -> 5,12*
              f1(3,14,1) -> 5,12*
              f1(1,14,2) -> 5,12*
              f1(2,1,14) -> 5,12*
              f1(3,1,3) -> 12*,5,10
              f1(3,16,1) -> 5,12*
              f1(1,16,2) -> 5,12*
              f1(2,3,14) -> 5,12*
              f1(3,3,3) -> 12*,5,10
              f1(14,1,1) -> 5,12*
              f1(14,3,1) -> 5,12*
              f1(4,1,1) -> 12*,5,10
              f1(2,1,2) -> 12*,5,10
              f1(4,3,1) -> 12*,5,10
              f1(2,3,2) -> 12*,5,10
              f1(14,2,3) -> 5,12*
              f1(3,2,14) -> 5,12*
              f1(14,4,3) -> 5,12*
              f1(4,2,3) -> 12*,5,10
              f1(3,4,14) -> 5,12*
              f1(4,4,3) -> 12*,5,10
              ok1(5) -> 5,12*
              ok1(12) -> 5,12*
            problem:
             strict:
              
             weak:
              f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
              active(f(a(),X,X)) -> mark(f(X,b(),b()))
              active(b()) -> mark(a())
              top(mark(X)) -> top(proper(X))
              proper(a()) -> ok(a())
              proper(b()) -> ok(b())
              f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
              top(ok(X)) -> top(active(X))
              active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
              proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
            Qed